﻿using System;
using System.Collections.Generic;
using System.Linq;
using TSU.FAMC.ComputerEngineering.Classes.BooleanMaths.Fundamental;
using TSU.FAMC.ComputerEngineering.Classes.Enums;
using System.IO;
using System.Collections;
using TSU.FAMC.ComputerEngineering.Classes.OrandTrees.Basis;

namespace TSU.FAMC.ComputerEngineering.Classes.OrandTrees
{
    /// <summary>
    /// ORAND-tree object in Boolean Mathematics.
    /// </summary>
    public class OrandTree : IEnumerable, ICloneable
    {
        // Properties

        /// <summary>
        /// Top vertices of the tree.
        /// </summary>
        public List<Vertex> Tops { get; private set; }

        /// <summary>
        /// Leaves of the tree.
        /// </summary>
        public List<Vertex> Leaves { get; private set; }

        /// <summary>
        /// List of input marsk determining circuit inputs order.
        /// </summary>
        public List<string> InputsOrder { get; set; }


        // Methods

        /// <summary>
        /// Default constructor.
        /// </summary>
        public OrandTree()
        {
            Tops = new List<Vertex>();
            Leaves = new List<Vertex>();
        }

        /// <summary>
        /// Normalizes and simplifies ORAND-tree be merging identical adjacent vertices, reducting mono-vertices with circuit elements number and appling all inversions.
        /// </summary>
        public void Simplify()
        {
            if (Tops.Count == 0)
            {
                // nothing to do
                return;
            }

            // applying inversion for all tops first!!!
            foreach (var top in Tops)
            {
                DoApplyInversion(top);
            }

            // reducing vertices encapsulating circuit's info (containing sequence of circuit elements).
            foreach (var top in Tops)
            {
                DoReduceInfoVertices(top);
            }

            // normalizing levels by merging identical adjacent vertices
            foreach (var top in Tops)
            {
                DoNormalizeLevels(top, null);
            }

            // removing one-to-one vertices
            var roundedVertices = new List<Vertex>();
            foreach (var top in Tops)
            {
                DoReduceOneToOneVertices(top, roundedVertices);
            }
        }

        /// <summary>
        /// Reduces redundant vertices encapsulating circuit information.
        /// </summary>
        /// <param name="currentElement">Current tree element.</param>
        private static void DoReduceInfoVertices(TreeElement currentElement)
        {
            var currentVertex = currentElement as Vertex;
            if (!ReferenceEquals(currentVertex, null) && currentVertex.Type == VertexType.Undefined)
            {
                // undefined vertex

                if (currentElement.Children.Count == 0)
                {
                    // nothing to do
                    return;
                }

                // removing it and falling down inversion sign
                foreach (var parentEdge in currentElement.Parents)
                {
                    parentEdge.Children.Remove(currentElement);
                    foreach (var childEdge in currentElement.Children)
                    {
                        parentEdge.Children.Add(childEdge.Children[0]);
                        childEdge.Children[0].Parents.Remove(childEdge);
                        childEdge.Children[0].Parents.Add(parentEdge);

                        // calculating new sign
                        var child = (Vertex) childEdge.Children[0];
                        child.IsInverted = child.IsInverted ^ currentVertex.IsInverted;

                        // appending edge data
                        if (parentEdge.Data is String)
                        {
                            parentEdge.Data += "," + childEdge.Data;
                        }

                        // going deep
                        DoReduceInfoVertices(child);
                    }
                }
                
                return;
            }

            // going deep
            var childrenCopy = new ElementInterface(currentElement.Children);
            foreach (var child in childrenCopy)
            {
                DoReduceInfoVertices(child);
            }
        }

        /// <summary>
        /// Normalizing tree levels by merging adjacent vertices of identical type AND->AND or OR->OR.
        /// </summary>
        /// <param name="currentElement">Currently rounding tree element.</param>
        /// <param name="parentVertex">Parent vertex in the tree for current location.</param>
        private static void DoNormalizeLevels(TreeElement currentElement, Vertex parentVertex)
        {
            ElementInterface listCopy;
            if (!(currentElement is Vertex))
            {
                // skipping an edge
                listCopy = new ElementInterface(currentElement.Children);
                foreach (var child in listCopy)
                {
                    DoNormalizeLevels(child, parentVertex);
                }

                return;
            }

            if (ReferenceEquals(parentVertex, null))
            {
                // skipping top vertex
                listCopy = new ElementInterface(currentElement.Children);
                foreach (var child in listCopy)
                {
                    DoNormalizeLevels(child, currentElement as Vertex);
                }

                return;
            }

            var currentVertex = currentElement as Vertex;
            if (ReferenceEquals(currentVertex, null))
            {
                // something wrong
                throw new InvalidDataException("Allowing only 2 types of tree elements: Edge and Vertex");
            }


            if (currentVertex.Type != VertexType.Input && parentVertex.Type != VertexType.Input &&
                currentVertex.Type != VertexType.Undefined && parentVertex.Type != VertexType.Undefined &&
                ((currentVertex.Type == parentVertex.Type && currentVertex.IsInverted == false) ||
                 (currentVertex.Type != parentVertex.Type && parentVertex.IsInverted == false && currentVertex.IsInverted)))
            {
                // identical vertices

                // searching for adjacent edge
                var adjacentEdge = currentVertex.Parents.FirstOrDefault(edge => ReferenceEquals(edge.Parents[0], parentVertex));

                if (ReferenceEquals(adjacentEdge, null))
                {
                    // something wrong
                    throw new InvalidDataException("Parent and current vertices must be connected with an edge.");
                }


                // merging vertices
                parentVertex.Children.Remove(adjacentEdge);
                currentVertex.Parents.Remove(adjacentEdge);
                adjacentEdge.Parents.Clear();
                adjacentEdge.Children.Clear();

                // appending current vertex children to parent vertex
                foreach (var child in currentVertex.Children)
                {
                    child.Parents.Remove(currentVertex);
                    child.Parents.Add(parentVertex);
                    parentVertex.Children.Add(child);
                    child.Data = (String)adjacentEdge.Data + "," + (String)child.Data;
                }

                // calculating new sign
                parentVertex.IsInverted = parentVertex.IsInverted ^ currentVertex.IsInverted;

                // setting current vertex as a result of merging
                currentVertex = parentVertex;
            }

            // going deeper into the tree
            listCopy = new ElementInterface(currentVertex.Children);
            foreach (var child in listCopy)
            {
                DoNormalizeLevels(child, currentVertex);
            }
        }


        /// <summary>
        /// Counts number of vertices in ORAND-tree object.
        /// </summary>
        /// <returns>Number of vertices.</returns>
        public int CountVertices()
        {
            var processedElements = new List<TreeElement>();
            return Tops.Sum(top => DoCountVertices(top, processedElements));
        }

        /// <summary>
        /// Counts number of vertices for current tree element by rounding tree recursively.
        /// </summary>
        /// <param name="currentElement">Current ORAND-tree element.</param>
        /// <param name="processedElements">Cache of processed elements.</param>
        /// <returns>Number of vertices in current subtree.</returns>
        private static int DoCountVertices(TreeElement currentElement, List<TreeElement> processedElements)
        {
            if (processedElements.Contains(currentElement))
            {
                return 0;
            }

            // caching
            processedElements.Add(currentElement);

            var subtreeVertexCount = currentElement.Children.Sum(child => DoCountVertices(child, processedElements));
            return currentElement is Vertex ? subtreeVertexCount + 1 : subtreeVertexCount;
        }

        /// <summary>
        /// Counts number of conjunctions in tree.
        /// </summary>
        /// <returns>Number of conjunctions.</returns>
        public long CountConjunctions()
        {
            return Tops.Sum(top => DoCountConjunctions(top));
        }

        /// <summary>
        /// Counts number of conjunctions in tree by roundin it recursively.
        /// </summary>
        /// <param name="currentVertex">Currently rounding element</param>
        /// <returns>Number of conjunctions in current subtree.</returns>
        private static long DoCountConjunctions(Vertex currentVertex)
        {
            var children = currentVertex.Children.Select(edge => edge.Children[0]).Cast<Vertex>();

            long conjunctions = 0;
            switch (currentVertex.Type)
            {
                case VertexType.And:
                    conjunctions = children.Aggregate<Vertex, long>(1, (current, child) => current*DoCountConjunctions(child));
                    break;
                case VertexType.Or:
                    conjunctions = children.Sum(child => DoCountConjunctions(child));
                    break;
                case VertexType.Input:
                    conjunctions = 1;
                    break;
                case VertexType.Constant0:
                case VertexType.Constant1:
                    throw new InvalidDataException("Tree contains constants, please reduce constants first.");
            }

            return conjunctions;
        }

        /// <summary>
        /// Gets a path string for specified leaf. Path contains of circuit elements names splitted by ',' sign.
        /// </summary>
        /// <param name="leaf">Leaf to get path for.</param>
        /// <returns>String representing circuit path.</returns>
        public string GetPath(Vertex leaf)
        {
            if (Leaves.IndexOf(leaf) == -1)
            {
                throw new InvalidDataException("Specified vertex does not belong to tree leaves");
            }

            var path = String.Empty;
            TreeElement parent = leaf;
            while (parent.Parents.Count > 0)
            {
                parent = parent.Parents[0];

                if (!(parent is Edge)) continue;

                if (path == String.Empty)
                {
                    path = parent.Data as string;
                }
                else
                {
                    path = parent.Data + "," + path;
                }
            }

            // appending to vertex data
            path = parent.Data + "," + path;
            return path;
        }

        /// <summary>
        /// Gets a path list for specified leaf.
        /// </summary>
        /// <param name="leaf">Leaf to get path for.</param>
        /// <returns>List of path elements.</returns>
        public List<string> GetPathList(Vertex leaf)
        {
            if (Leaves.IndexOf(leaf) == -1)
            {
                throw new InvalidDataException("Specified vertex does not belong to tree leaves");
            }

            var path = String.Empty;
            TreeElement parent = leaf;
            while (parent.Parents.Count > 0)
            {
                parent = parent.Parents[0];

                if (!(parent is Edge)) continue;

                if (path == String.Empty)
                {
                    path = parent.Data as string;
                }
                else
                {
                    path = parent.Data + "," + path;
                }
            }

            // appending to vertex data
            path = parent.Data + "," + path;
            return path.Split(new[] {','}).ToList();
        }

        /// <summary>
        /// Returns ORAND-tree enumerator. Enumeration only allowed for one-top trees.
        /// </summary>
        /// <returns>ORAND-tree enumerator</returns>
        IEnumerator IEnumerable.GetEnumerator()
        {
            if (Tops.Count != 1)
            {
                throw new InvalidOperationException("Enumeration only allowed for one-top trees");
            }

            return new OrandTreeEnum(this);
        }

        /// <summary>
        /// Clones tree.
        /// </summary>
        /// <returns>Identical OrandTree</returns>
        public object Clone()
        {
            var clone = new OrandTree();
            var elementsCache = new Dictionary<TreeElement, TreeElement>();
            foreach (var top in Tops)
            {
                DoClone(top, elementsCache);
            }

            // setting tops and leaves
            foreach (var top in Tops)
            {
                var clonedTop = (Vertex)elementsCache[top];
                clone.Tops.Add(clonedTop);
            }

            foreach (var leaf in Leaves)
            {
                var clonedLeaf = (Vertex)elementsCache[leaf];
                clone.Leaves.Add(clonedLeaf);
            }

            // cloning order
            if (InputsOrder != null)
            {
                clone.InputsOrder = new List<string>(InputsOrder);
            }

            return clone;
        }

        /// <summary>
        /// Clones tree by rounding it recursively.
        /// </summary>
        /// <param name="currentElement">Currently rounding tree element.</param>
        /// <param name="elementsCache">Already created elements.</param>
        private static TreeElement DoClone(TreeElement currentElement, IDictionary<TreeElement, TreeElement> elementsCache)
        {
            // checking cache
            var search = elementsCache.Where(e => ReferenceEquals(e.Key, currentElement)).ToList();
            if (search.Count > 0)
            {
                return search.First().Value;
            }

            // cloning element
            var clonedElement = (TreeElement)currentElement.Clone();
            clonedElement.Parents.Clear();
            clonedElement.Children.Clear();

            // caching
            elementsCache.Add(currentElement, clonedElement);


            // going down
            foreach (var clonedChild in currentElement.Children.Select(child => DoClone(child, elementsCache)))
            {
                clonedElement.LinkChild(clonedChild);
            }

            return clonedElement;
        }

        /// <summary>
        /// Destroys tree object.
        /// </summary>
        public void Destroy()
        {
            foreach (var top in Tops)
            {
                top.Destroy();
            }

            Tops.Clear();
            Leaves.Clear();
        }

        /// <summary>
        /// Inverts tree.
        /// </summary>
        public void Invert()
        {
            // inverting tops
            foreach (var top in Tops)
            {
                top.IsInverted = !top.IsInverted;
            }

            // applying inversion for all tops
            foreach (var top in Tops)
            {
                DoApplyInversion(top);
            }
        }

        /// <summary>
        /// Applies inversion from top to bottom by inverting types of vertices and drops inversion in leaves.
        /// </summary>
        /// <param name="currentVertex">Currently inverting vertex.</param>
        /// <param name="signOfInversion">Current sing of the inversion.</param>
        private static void DoApplyInversion(Vertex currentVertex, bool signOfInversion = false)
        {
            if (currentVertex.Children.Count == 0)
            {
                // leaf
                currentVertex.IsInverted = currentVertex.IsInverted ^ signOfInversion;
                return;
            }

            // internal vertex
            if (currentVertex.IsInverted == signOfInversion)
            {
                // inversion cancellation
                currentVertex.IsInverted = false;
                signOfInversion = false;
            }
            else
            {
                // inverting vertex type
                switch (currentVertex.Type)
                {
                    case VertexType.And:
                        currentVertex.Type = VertexType.Or;
                        break;
                    case VertexType.Or:
                        currentVertex.Type = VertexType.And;
                        break;
                    case VertexType.Constant0:
                        currentVertex.Type = VertexType.Constant1;
                        break;
                    case VertexType.Constant1:
                        currentVertex.Type = VertexType.Constant0;
                        break;
                }

                currentVertex.IsInverted = false;
                signOfInversion = true;
            }


            // going down
            foreach (Vertex child in currentVertex.Children.Select(edge => edge.Children[0]))
            {
                DoApplyInversion(child, signOfInversion);
            }
        }

        /// <summary>
        /// Performs equivalent transformations on the tree by reducting constants.
        /// </summary>
        public void ReduceConstants()
        {
            var roundedVertices = new List<Vertex>();

            // removing one-to-one vertices
            var topsCopy = new List<Vertex>(Tops);
            foreach (var top in topsCopy)
            {
                DoReduceOneToOneVertices(top, roundedVertices);
            }

            // reducing constants
            roundedVertices.Clear();
            topsCopy = new List<Vertex>(Tops);
            foreach (var top in topsCopy)
            {
                DoReduceConstants(top, roundedVertices);
            }

            // removing one-to-one vertices aftter reduction
            roundedVertices.Clear();
            topsCopy = new List<Vertex>(Tops);
            foreach (var top in topsCopy)
            {
                DoReduceOneToOneVertices(top, roundedVertices);
            }

            // normalizing levels by merging identical adjacent vertices
            roundedVertices.Clear();
            topsCopy = new List<Vertex>(Tops);
            foreach (var top in topsCopy)
            {
                DoNormalizeLevels(top, null);
            }

            // removing reduced leaves
            foreach (var leaf in new List<Vertex>(Leaves).Where(leaf => leaf.Parents.Count == 0 && !Tops.Contains(leaf)))
            {
                Leaves.Remove(leaf);
            }
        }

        /// <summary>
        /// Performs constant reduction by rounding tree.
        /// </summary>
        /// <param name="currentVertex">Currently rounded vertex.</param>
        /// <param name="roundedVertices">Already rounded vertices.</param>
        private void DoReduceConstants(Vertex currentVertex, List<Vertex> roundedVertices)
        {
            if (roundedVertices.Contains(currentVertex))
            {
                // already evaludated
                return;
            }

            // memorizing
            roundedVertices.Add(currentVertex);

            // going down
            var children = currentVertex.Children.Select(edge => edge.Children[0]).ToList();
            Vertex lastConstantChild = null;
            for (var i = 0; i < children.Count; i++)
            {
                var child = (Vertex)children[i];

                if ((child.Type == VertexType.Constant0 && !child.IsInverted) ||
                    (child.Type == VertexType.Constant1 && child.IsInverted))
                {
                    lastConstantChild = child;

                    if ((currentVertex.Type == VertexType.Or && !currentVertex.IsInverted) ||
                        (currentVertex.Type == VertexType.And && currentVertex.IsInverted))
                    {
                        // removing child with it's edge
                        currentVertex.UnlinkVertex(child);

                        // destroying subtree
                        child.Destroy();
                    }
                    else if ((currentVertex.Type == VertexType.And && !currentVertex.IsInverted) ||
                             (currentVertex.Type == VertexType.Or && currentVertex.IsInverted))
                    {
                        if (currentVertex.Parents.Count > 0)
                        {
                            // unlinking all subtree from parent vertices
                            foreach (Vertex parent in currentVertex.Parents.Select(edge => edge.Parents[0]).ToList())
                            {
                                parent.UnlinkVertex(currentVertex);
                                currentVertex.UnlinkVertex(child);
                                parent.LinkChildVertex(lastConstantChild);
                            }

                            // destroying subtree
                            currentVertex.Destroy();
                            break;
                        }

                        // no parents, constant tree
                        Destroy();

                        Tops.Add(child);
                        Leaves.Add(child);
                        return;
                    }
                }
                else if ((child.Type == VertexType.Constant1 && !child.IsInverted) ||
                         (child.Type == VertexType.Constant0 && child.IsInverted))
                {
                    lastConstantChild = child;

                    if ((currentVertex.Type == VertexType.And && !currentVertex.IsInverted) ||
                        (currentVertex.Type == VertexType.Or && currentVertex.IsInverted))
                    {
                        // removing child with it's edge
                        currentVertex.UnlinkVertex(child);

                        // destroying subtree
                        child.Destroy();
                    }
                    else if ((currentVertex.Type == VertexType.Or && !currentVertex.IsInverted) ||
                             (currentVertex.Type == VertexType.And && currentVertex.IsInverted))
                    {
                        if (currentVertex.Parents.Count > 0)
                        {
                            // unlinking all subtree from parent vertices
                            foreach (Vertex parent in currentVertex.Parents.Select(edge => edge.Parents[0]).ToList())
                            {
                                parent.UnlinkVertex(currentVertex);
                                currentVertex.UnlinkVertex(child);
                                parent.LinkChildVertex(lastConstantChild);
                            }

                            // destroying subtree
                            currentVertex.Destroy();
                            break;
                        }

                        // no parents, constant tree
                        Destroy();

                        Tops.Add(child);
                        Leaves.Add(child);
                        return;
                    }
                }
                else
                {
                    // going down in child subtee
                    DoReduceConstants(child, roundedVertices);

                    if (child.Parents.Count == 0)
                    {
                        // child has been modified, executing reduction on vertex children again
                        children = currentVertex.Children.Select(edge => edge.Children[0]).ToList();
                        i = -1;
                    }
                }

                // checking whether there are no children left
                if (currentVertex.Children.Count != 0 || lastConstantChild == null) continue;

                // replacing inner vertex within last constant child
                if (currentVertex.Parents.Count == 0)
                {
                    // top vertex
                    Destroy();
                    Tops.Add(child);
                    Leaves.Add(child);
                }
                else
                {
                    // inner vertex
                    foreach (Vertex parent in currentVertex.Parents.Select(edge => edge.Parents[0]).ToList())
                    {
                        parent.UnlinkVertex(currentVertex);
                        parent.LinkChildVertex(lastConstantChild);
                    }
                }
            }
        }

        /// <summary>
        /// Eleminates one-to-one vertices by removing such a vertex with following appending child vertex.
        /// </summary>
        public void ReduceOneToOneVertices()
        {
            var roundedVertices = new List<Vertex>();
            foreach (var top in Tops)
            {
                DoReduceOneToOneVertices(top, roundedVertices);
            }
        }

        /// <summary>
        /// Performs one-to-one vertices reduction by rounding tree.
        /// </summary>
        /// <param name="currentVertex">Currently rounded vertex.</param>
        /// <param name="roundedVertices">Already rounded vertices.</param>
        private static void DoReduceOneToOneVertices(Vertex currentVertex, List<Vertex> roundedVertices)
        {
            if (roundedVertices.Contains(currentVertex))
            {
                // already evaluated
                return;
            }

            // memorizing
            roundedVertices.Add(currentVertex);

            // reducing for non-root vertex
            if (currentVertex.Parents.Count > 0 && currentVertex.Children.Count == 1)
            {
                // one child edge, should be removed
                var singleChild = (Vertex) currentVertex.Children[0].Children[0];
                foreach (Vertex parent in currentVertex.Parents.Select(edge => edge.Parents[0]).ToList())
                {
                    currentVertex.UnlinkVertex(singleChild);
                    parent.UnlinkVertex(currentVertex);
                    parent.LinkChildVertex(singleChild);
                }

                return;
            }

            // going down
            var children = currentVertex.Children.Select(edge => edge.Children[0]).ToList();
            for (var i = 0; i < children.Count; i++)
            {
                var child = (Vertex)children[i];
                DoReduceOneToOneVertices(child, roundedVertices);

                if (child.Parents.Count == 0)
                {
                    // child modified, repeat again
                    children = currentVertex.Children.Select(edge => edge.Children[0]).ToList();
                    i = -1;
                    continue;
                }
            }
        }

        /// <summary>
        /// Returns a part of original tree containing only conjunctions with specified path.
        /// </summary>
        /// <param name="pathLeaf">The tree leaf determining circuit path.</param>
        /// <returns>Path tree.</returns>
        public OrandTree PathSensitization(Vertex pathLeaf)
        {
            if (!Leaves.Contains(pathLeaf))
            {
                throw new InvalidDataException("Specified vertex is not a leaf of the tree.");
            }

            // cloning tree
            var clone = (OrandTree) Clone();

            // simplifying tree
            clone.Simplify();

            var processedVertices = new List<Vertex>();
            var clonedPathLeaf = clone.Leaves[Leaves.IndexOf(pathLeaf)];
            DoPathSensitization(clonedPathLeaf, processedVertices);

            // removing reduced leaves
            foreach (var leaf in new List<Vertex>(clone.Leaves).Where(leaf => !clone.Tops.Contains(leaf) && leaf.Parents.Count == 0))
            {
                clone.Leaves.Remove(leaf);
            }

            return clone;
        }

        /// <summary>
        /// Isolates subtree sensitizes specified leaf-path by rounding it from leaf to tops.
        /// </summary>
        /// <param name="currentVertex">Currenttly rounding vertex of the tree.</param>
        /// <param name="processedVertices">Already evaludated vertices.</param>
        private static void DoPathSensitization(Vertex currentVertex, List<Vertex> processedVertices)
        {
            foreach (var parent in
                currentVertex.Parents.Select(edge => edge.Parents[0]).ToList().Cast<Vertex>().Where(parent => !processedVertices.Contains(parent)))
            {
                // memorizing parent
                processedVertices.Add(parent);

                if (parent.Type == VertexType.Or)
                {
                    // removing all subtrees except current
                    foreach (
                        Vertex anotherChild in
                            parent.Children.Select(edge => edge.Children[0]).Where(
                                v => !ReferenceEquals(v, currentVertex)).ToList())
                    {
                        // unlinking another child from parent
                        parent.UnlinkVertex(anotherChild);
                        anotherChild.Destroy();
                    }
                }

                // going up
                DoPathSensitization(parent, processedVertices);
            }
        }

        /// <summary>
        /// Returns a part of original tree without path-relative subtree.
        /// </summary>
        /// <param name="pathLeaf">The tree leaf determining circuit path.</param>
        /// <returns>A tree without path.</returns>
        public OrandTree ExcludePath(Vertex pathLeaf)
        {
            if (!Leaves.Contains(pathLeaf))
            {
                throw new InvalidDataException("Specified vertex is not a leaf of the tree.");
            }

            // cloning tree
            var clone = (OrandTree)Clone();

            // simplifying tree
            clone.Simplify();

            var processedVertices = new List<Vertex>();
            var clonedPathLeaf = clone.Leaves[Leaves.IndexOf(pathLeaf)];
            DoExcludePath(clonedPathLeaf, processedVertices);

            // removing reduced leaves
            foreach (var leaf in new List<Vertex>(clone.Leaves).Where(leaf => !clone.Tops.Contains(leaf) && leaf.Parents.Count == 0))
            {
                clone.Leaves.Remove(leaf);
            }

            return clone;
        }

        /// <summary>
        /// Removes path-relative sub-tree from tree.
        /// </summary>
        /// <param name="currentVertex">Currenttly rounding vertex of the tree.</param>
        /// <param name="processedVertices">Already evaludated vertices.</param>
        private static void DoExcludePath(Vertex currentVertex, List<Vertex> processedVertices)
        {
            foreach (var parent in
                currentVertex.Parents.Select(edge => edge.Parents[0]).ToList().Cast<Vertex>().Where(parent => !processedVertices.Contains(parent)))
            {
                // memorizing parent
                processedVertices.Add(parent);

                if (parent.Type == VertexType.Or)
                {
                    // removing subtrees
                    parent.UnlinkVertex(currentVertex);
                    currentVertex.Destroy();
                    return;
                }

                // going up
                DoExcludePath(parent, processedVertices);
            }
        }

        /// <summary>
        /// Returns order of input marks.
        /// </summary>
        /// <returns>List of input marks used in tree.</returns>
        public List<string> GetInputsOrder()
        {
            var inputMarks = new List<string>();
            foreach (var leaf in Leaves)
            {
                var inputMark = GetInputMark(leaf);
                if (inputMarks.Contains(inputMark))
                {
                    continue;
                }

                inputMarks.Add(inputMark);
            }

            return inputMarks;
        }

        /// <summary>
        /// Fixes input variables by replacing leaf vertices with constants.
        /// Variables input indices assigned to leaf.Data property to save input information.
        /// </summary>
        /// <param name="inputs">Cube, representing input values.</param>
        public void FixInputs(Cube inputs)
        {
            var inputsOrder = InputsOrder != null && InputsOrder.Count > 0 ? InputsOrder : GetInputsOrder();
            foreach (var leaf in Leaves)
            {
                var inputMark = GetInputMark(leaf);
                var index = inputsOrder.IndexOf(inputMark);
                leaf.Data = inputMark;

                if (inputs[index] == BooleanValue.True)
                {
                    leaf.Type = !leaf.IsInverted ? VertexType.Constant1 : VertexType.Constant0;
                    leaf.IsInverted = false;
                }
                else if (inputs[index] == BooleanValue.False)
                {
                    leaf.Type = !leaf.IsInverted ? VertexType.Constant0 : VertexType.Constant1;
                    leaf.IsInverted = false;
                }
                else
                {
                    continue;
                }
            }

            // reducing constants
            ReduceConstants();
        }

        /// <summary>
        /// Returns the mark of input corresponging to input for leaf vertex of the tree.
        /// </summary>
        /// <param name="leaf">Leaf vertex of the tree to get input mark for.</param>
        /// <returns>Input mark.</returns>
        public static string GetInputMark(Vertex leaf)
        {
            // retreiving input index
            if (leaf.Children.Count != 0)
            {
                throw new InvalidDataException("Specified vertex is not a valid tree leaf.");
            }

            string inputNumberStr = null;
            if (leaf.Data != null)
            {
                // retrieving data from leaf object
                inputNumberStr = leaf.Data.ToString();
            }
            else if (leaf.Parents.Count > 0)
            {
                // retrieving data from parent edge
                var parentEdge = leaf.Parents[0];
                inputNumberStr = parentEdge.Data as String;
            }

            if (inputNumberStr == null)
            {
                inputNumberStr = String.Empty;
            }

            var dlms = new[] { "," };
            var marks = inputNumberStr.Split(dlms, Int32.MaxValue, StringSplitOptions.RemoveEmptyEntries);

            return marks.Length > 0 ? marks[marks.Length - 1] : null;
        }

        /// <summary>
        /// Extracts subtree with a top vertex specified.
        /// </summary>
        /// <param name="top">Subtree top vertex.</param>
        /// <returns>Cloned subtree.</returns>
        public OrandTree ExtractTree(Vertex top)
        {
            var clone = new OrandTree();
            var elementsCache = new Dictionary<TreeElement, TreeElement>();

            // cloning
            DoClone(top, elementsCache);

            // setting top
            clone.Tops.Add((Vertex)elementsCache[top]);

            // setting leaves
            foreach (var clonedLeaf in Leaves.Where(elementsCache.ContainsKey).Select(leaf => elementsCache[leaf]).OfType<Vertex>())
            {
                clone.Leaves.Add(clonedLeaf);
            }

            return clone;
        }
    }


    public class OrandTreeEnum : IEnumerator
    {
        // Properties

        /// <summary>
        /// ORAND-tree object to enumerate.
        /// </summary>
        private readonly OrandTree _tree;

        /// <summary>
        /// Enumerator position.
        /// </summary>
        int _position = -1;

        /// <summary>
        /// Next found conjunction.
        /// </summary>
        private ElementInterface _nextConjunction;

        /// <summary>
        /// Offsets for OR vertices to know which child will be next.
        /// </summary>
        private readonly Dictionary<Vertex, int> _vertexOffsets;

        /// <summary>
        /// Indicates whether offsets changed during tree rounding.
        /// </summary>
        private bool _offsetsChanged;


        // Methods

        /// <summary>
        /// Constructor.
        /// </summary>
        /// <param name="tree">OrandTree object.</param>
        public OrandTreeEnum(OrandTree tree)
        {
            _tree = tree;
            _nextConjunction = new ElementInterface();
            _vertexOffsets = new Dictionary<Vertex, int>();
        }

        /// <summary>
        /// Moves enumerator position next.
        /// </summary>
        /// <returns>Returns true if there are some elements next.</returns>
        public bool MoveNext()
        {
            _position++;

            _offsetsChanged = false;
            _nextConjunction.Clear();

            // rounding tree
            DoRound(_tree.Tops[0], false);

            return _offsetsChanged;
        }

        /// <summary>
        /// Resets enumberator position.
        /// </summary>
        public void Reset()
        {
            _position = -1;
            _vertexOffsets.Clear();
        }

        /// <summary>
        /// Returns current object of the enumerable object.
        /// </summary>
        public object Current
        {
            get
            {
                // getting current element
                return new ElementInterface(_nextConjunction);
            }
        }

        /// <summary>
        /// Makes rounding of the tree, starting from specified vertex.
        /// </summary>
        /// <param name="currentElement">Currently rounding tree element.</param>
        /// <param name="inversion">Current inversion.</param>
        private void DoRound(TreeElement currentElement, bool inversion)
        {
            if (currentElement.Parents.Count == 0 && _vertexOffsets.Count == 0 && _position == 0)
            {
                // top of the tree and first call
                _offsetsChanged = true;
            }

            if (!(currentElement is Vertex))
            {
                // skipping edge

                if (currentElement.Children.Count != 0)
                {
                    DoRound(currentElement.Children[0], inversion);
                }

                return;
            }


            var currentVertex = currentElement as Vertex;
            if ((currentVertex.Type == VertexType.Or && (currentVertex.IsInverted ^ inversion) == false) ||
                (currentVertex.Type == VertexType.And && (currentVertex.IsInverted ^ inversion)))
            {
                // OR vertex, going to child according to offset

                if (!_vertexOffsets.ContainsKey(currentVertex))
                {
                    // first time, creating zero offset
                    _vertexOffsets.Add(currentVertex, 0);
                    _offsetsChanged = true;
                }

                // retreiving current offset
                var currentOffset = _vertexOffsets[currentVertex];

                // going deeper
                var copyConjunction = new ElementInterface(_nextConjunction);
                DoRound(currentVertex.Children[currentOffset], currentVertex.IsInverted ^ inversion);

                if (!_offsetsChanged)
                {
                    // making rollback
                    _nextConjunction = copyConjunction;


                    // trying use next offset or reset offset
                    if (currentVertex.Children.Count == currentOffset + 1)
                    {
                        // it was the last child, reseting offset
                        _vertexOffsets.Remove(currentVertex);
                        _vertexOffsets.Add(currentVertex, 0);

                        _offsetsChanged = true;
                        DoRound(currentVertex.Children[0], currentVertex.IsInverted ^ inversion);
                        _offsetsChanged = false;
                    }
                    else
                    {
                        // incrementing offset
                        currentOffset++;
                        _vertexOffsets.Remove(currentVertex);
                        _vertexOffsets.Add(currentVertex, currentOffset);

                        _offsetsChanged = true;

                        // going deeper
                        DoRound(currentVertex.Children[currentOffset], currentVertex.IsInverted ^ inversion);
                    }
                }


                return;
            }

            // And vertex, going to the children
            foreach (var child in currentVertex.Children)
            {
                DoRound(child, currentVertex.IsInverted ^ inversion);
            }


            if (currentVertex.Children.Count != 0) return;

            // memorizing leaf
            var toConjunctionLeaf = new Vertex
                                        {
                                            Type = currentVertex.Type,
                                            IsInverted = currentVertex.IsInverted ^ inversion,
                                            RelatedElement = currentVertex
                                        };

            // retreiving input mark
            if (currentVertex.Type == VertexType.Input)
            {
                // input variable vertex, getting input index
                toConjunctionLeaf.Data = OrandTree.GetInputMark(currentVertex);
            }

            _nextConjunction.Add(toConjunctionLeaf);
        }
    }

}
